; ModuleID = '/home/shadowvm/shadow/bupt_use_update/bupt_use/runtime/Intrinsic/klee_mark_arg_symbolic.c'
target datalayout = "e-p:64:64:64-i1:8:8-i8:8:8-i16:16:16-i32:32:32-i64:64:64-f32:32:32-f64:64:64-v64:64:64-v128:128:128-a0:0:64-s0:64:64-f80:128:128-n8:16:32:64-S128"
target triple = "x86_64-unknown-linux-gnu"

@.str = private unnamed_addr constant [5 x i8] c"argv\00", align 1

; Function Attrs: nounwind uwtable
define void @klee_mark_arg_symbolic(i32 %argc, i8** nocapture readonly %argv) #0 {
entry:
  tail call void @llvm.dbg.value(metadata !{i32 %argc}, i64 0, metadata !13), !dbg !33
  tail call void @llvm.dbg.value(metadata !{i8** %argv}, i64 0, metadata !14), !dbg !33
  tail call void @llvm.dbg.value(metadata !34, i64 0, metadata !15), !dbg !35
  %cmp49 = icmp sgt i32 %argc, 1, !dbg !35
  br i1 %cmp49, label %for.body, label %for.end29, !dbg !35

for.body:                                         ; preds = %entry, %for.end
  %indvars.iv52 = phi i64 [ %indvars.iv.next53, %for.end ], [ 1, %entry ]
  %arrayidx = getelementptr inbounds i8** %argv, i64 %indvars.iv52, !dbg !37
  %0 = load i8** %arrayidx, align 8, !dbg !37, !tbaa !39
  tail call void @llvm.dbg.value(metadata !{i8* %0}, i64 0, metadata !43), !dbg !44
  tail call void @llvm.dbg.value(metadata !2, i64 0, metadata !45), !dbg !46
  br label %while.cond.i, !dbg !47

while.cond.i:                                     ; preds = %while.cond.i, %for.body
  %indvars.iv.i = phi i64 [ %indvars.iv.next.i, %while.cond.i ], [ 0, %for.body ]
  %i.0.i = phi i32 [ %inc.i, %while.cond.i ], [ 0, %for.body ]
  %indvars.iv.next.i = add nuw nsw i64 %indvars.iv.i, 1, !dbg !47
  %inc.i = add nsw i32 %i.0.i, 1, !dbg !47
  tail call void @llvm.dbg.value(metadata !{i32 %inc.i}, i64 0, metadata !45), !dbg !47
  %arrayidx.i = getelementptr inbounds i8* %0, i64 %indvars.iv.i, !dbg !47
  %1 = load i8* %arrayidx.i, align 1, !dbg !47, !tbaa !48
  %tobool.i = icmp eq i8 %1, 0, !dbg !47
  br i1 %tobool.i, label %my_strlen.exit, label %while.cond.i, !dbg !47

my_strlen.exit:                                   ; preds = %while.cond.i
  tail call void @llvm.dbg.value(metadata !{i32 %i.0.i}, i64 0, metadata !17), !dbg !37
  %conv = sext i32 %inc.i to i64, !dbg !49
  tail call void @klee_make_symbolic(i8* %0, i64 %conv, i8* getelementptr inbounds ([5 x i8]* @.str, i64 0, i64 0)) #3, !dbg !49
  %idxprom3 = sext i32 %i.0.i to i64, !dbg !50
  %2 = load i8** %arrayidx, align 8, !dbg !50, !tbaa !39
  %arrayidx6 = getelementptr inbounds i8* %2, i64 %idxprom3, !dbg !50
  %3 = load i8* %arrayidx6, align 1, !dbg !50, !tbaa !48
  %cmp8 = icmp eq i8 %3, 0, !dbg !50
  %conv10 = zext i1 %cmp8 to i64, !dbg !50
  tail call void @klee_assume(i64 %conv10) #3, !dbg !50
  tail call void @llvm.dbg.value(metadata !2, i64 0, metadata !16), !dbg !51
  %cmp1247 = icmp sgt i32 %i.0.i, 0, !dbg !51
  %4 = load i8** %arrayidx, align 8, !dbg !53, !tbaa !39
  br i1 %cmp1247, label %for.body14, label %for.end, !dbg !51

for.body14:                                       ; preds = %my_strlen.exit, %for.body14
  %indvars.iv = phi i64 [ %indvars.iv.next, %for.body14 ], [ 0, %my_strlen.exit ]
  %5 = phi i8* [ %7, %for.body14 ], [ %4, %my_strlen.exit ]
  %arrayidx20 = getelementptr inbounds i8* %5, i64 %indvars.iv, !dbg !53
  %6 = load i8* %arrayidx20, align 1, !dbg !53, !tbaa !48
  tail call void @llvm.dbg.value(metadata !{i8 %6}, i64 0, metadata !55), !dbg !56
  %cmp.i = icmp sgt i8 %6, 31, !dbg !57
  %cmp3.i = icmp ne i8 %6, 127, !dbg !57
  %cmp3..i = and i1 %cmp.i, %cmp3.i, !dbg !57
  %conv22 = zext i1 %cmp3..i to i64, !dbg !53
  tail call void @klee_prefer_cex(i8* %5, i64 %conv22) #3, !dbg !53
  %indvars.iv.next = add nuw nsw i64 %indvars.iv, 1, !dbg !51
  %7 = load i8** %arrayidx, align 8, !dbg !53, !tbaa !39
  %lftr.wideiv = trunc i64 %indvars.iv.next to i32, !dbg !51
  %exitcond = icmp eq i32 %lftr.wideiv, %i.0.i, !dbg !51
  br i1 %exitcond, label %for.end, label %for.body14, !dbg !51

for.end:                                          ; preds = %for.body14, %my_strlen.exit
  %.lcssa = phi i8* [ %4, %my_strlen.exit ], [ %7, %for.body14 ]
  %arrayidx26 = getelementptr inbounds i8* %.lcssa, i64 %idxprom3, !dbg !58
  store i8 0, i8* %arrayidx26, align 1, !dbg !58, !tbaa !48
  %indvars.iv.next53 = add nuw nsw i64 %indvars.iv52, 1, !dbg !35
  %lftr.wideiv54 = trunc i64 %indvars.iv.next53 to i32, !dbg !35
  %exitcond55 = icmp eq i32 %lftr.wideiv54, %argc, !dbg !35
  br i1 %exitcond55, label %for.end29, label %for.body, !dbg !35

for.end29:                                        ; preds = %for.end, %entry
  ret void, !dbg !59
}

declare void @klee_make_symbolic(i8*, i64, i8*) #1

declare void @klee_assume(i64) #1

declare void @klee_prefer_cex(i8*, i64) #1

; Function Attrs: nounwind readnone
declare void @llvm.dbg.value(metadata, i64, metadata) #2

attributes #0 = { nounwind uwtable "less-precise-fpmad"="false" "no-frame-pointer-elim"="false" "no-infs-fp-math"="false" "no-nans-fp-math"="false" "stack-protector-buffer-size"="8" "unsafe-fp-math"="false" "use-soft-float"="false" }
attributes #1 = { "less-precise-fpmad"="false" "no-frame-pointer-elim"="false" "no-infs-fp-math"="false" "no-nans-fp-math"="false" "stack-protector-buffer-size"="8" "unsafe-fp-math"="false" "use-soft-float"="false" }
attributes #2 = { nounwind readnone }
attributes #3 = { nobuiltin nounwind }

!llvm.dbg.cu = !{!0}
!llvm.module.flags = !{!30, !31}
!llvm.ident = !{!32}

!0 = metadata !{i32 786449, metadata !1, i32 1, metadata !"clang version 3.4 (tags/RELEASE_34/final)", i1 true, metadata !"", i32 0, metadata !2, metadata !2, metadata !3, metadata !2, metadata !2, metadata !""} ; [ DW_TAG_compile_unit ] [/home/shadowvm/shadow/bupt_use_update/bupt_use/build_3/runtime/Intrinsic//home/shadowvm/shadow/bupt_use_update/bupt_use/runtime/Intrinsic/klee_mark_arg_symbolic.c] [DW_LANG_C89]
!1 = metadata !{metadata !"/home/shadowvm/shadow/bupt_use_update/bupt_use/runtime/Intrinsic/klee_mark_arg_symbolic.c", metadata !"/home/shadowvm/shadow/bupt_use_update/bupt_use/build_3/runtime/Intrinsic"}
!2 = metadata !{i32 0}
!3 = metadata !{metadata !4, metadata !18, metadata !24}
!4 = metadata !{i32 786478, metadata !1, metadata !5, metadata !"klee_mark_arg_symbolic", metadata !"klee_mark_arg_symbolic", metadata !"", i32 23, metadata !6, i1 false, i1 true, i32 0, i32 0, null, i32 256, i1 true, void (i32, i8**)* @klee_mark_arg_symbolic, null, null, metadata !12, i32 23} ; [ DW_TAG_subprogram ] [line 23] [def] [klee_mark_arg_symbolic]
!5 = metadata !{i32 786473, metadata !1}          ; [ DW_TAG_file_type ] [/home/shadowvm/shadow/bupt_use_update/bupt_use/build_3/runtime/Intrinsic//home/shadowvm/shadow/bupt_use_update/bupt_use/runtime/Intrinsic/klee_mark_arg_symbolic.c]
!6 = metadata !{i32 786453, i32 0, null, metadata !"", i32 0, i64 0, i64 0, i64 0, i32 0, null, metadata !7, i32 0, null, null, null} ; [ DW_TAG_subroutine_type ] [line 0, size 0, align 0, offset 0] [from ]
!7 = metadata !{null, metadata !8, metadata !9}
!8 = metadata !{i32 786468, null, null, metadata !"int", i32 0, i64 32, i64 32, i64 0, i32 0, i32 5} ; [ DW_TAG_base_type ] [int] [line 0, size 32, align 32, offset 0, enc DW_ATE_signed]
!9 = metadata !{i32 786447, null, null, metadata !"", i32 0, i64 64, i64 64, i64 0, i32 0, metadata !10} ; [ DW_TAG_pointer_type ] [line 0, size 64, align 64, offset 0] [from ]
!10 = metadata !{i32 786447, null, null, metadata !"", i32 0, i64 64, i64 64, i64 0, i32 0, metadata !11} ; [ DW_TAG_pointer_type ] [line 0, size 64, align 64, offset 0] [from char]
!11 = metadata !{i32 786468, null, null, metadata !"char", i32 0, i64 8, i64 8, i64 0, i32 0, i32 6} ; [ DW_TAG_base_type ] [char] [line 0, size 8, align 8, offset 0, enc DW_ATE_signed_char]
!12 = metadata !{metadata !13, metadata !14, metadata !15, metadata !16, metadata !17}
!13 = metadata !{i32 786689, metadata !4, metadata !"argc", metadata !5, i32 16777239, metadata !8, i32 0, i32 0} ; [ DW_TAG_arg_variable ] [argc] [line 23]
!14 = metadata !{i32 786689, metadata !4, metadata !"argv", metadata !5, i32 33554455, metadata !9, i32 0, i32 0} ; [ DW_TAG_arg_variable ] [argv] [line 23]
!15 = metadata !{i32 786688, metadata !4, metadata !"i", metadata !5, i32 24, metadata !8, i32 0, i32 0} ; [ DW_TAG_auto_variable ] [i] [line 24]
!16 = metadata !{i32 786688, metadata !4, metadata !"j", metadata !5, i32 24, metadata !8, i32 0, i32 0} ; [ DW_TAG_auto_variable ] [j] [line 24]
!17 = metadata !{i32 786688, metadata !4, metadata !"len", metadata !5, i32 24, metadata !8, i32 0, i32 0} ; [ DW_TAG_auto_variable ] [len] [line 24]
!18 = metadata !{i32 786478, metadata !1, metadata !5, metadata !"__isprint", metadata !"__isprint", metadata !"", i32 19, metadata !19, i1 true, i1 true, i32 0, i32 0, null, i32 256, i1 true, null, null, null, metadata !22, i32 19} ; [ DW_TAG_subprogram ] [line 19] [local] [def] [__isprint]
!19 = metadata !{i32 786453, i32 0, null, metadata !"", i32 0, i64 0, i64 0, i64 0, i32 0, null, metadata !20, i32 0, null, null, null} ; [ DW_TAG_subroutine_type ] [line 0, size 0, align 0, offset 0] [from ]
!20 = metadata !{metadata !8, metadata !21}
!21 = metadata !{i32 786470, null, null, metadata !"", i32 0, i64 0, i64 0, i64 0, i32 0, metadata !11} ; [ DW_TAG_const_type ] [line 0, size 0, align 0, offset 0] [from char]
!22 = metadata !{metadata !23}
!23 = metadata !{i32 786689, metadata !18, metadata !"c", metadata !5, i32 16777235, metadata !21, i32 0, i32 0} ; [ DW_TAG_arg_variable ] [c] [line 19]
!24 = metadata !{i32 786478, metadata !1, metadata !5, metadata !"my_strlen", metadata !"my_strlen", metadata !"", i32 13, metadata !25, i1 true, i1 true, i32 0, i32 0, null, i32 256, i1 true, null, null, null, metadata !27, i32 13} ; [ DW_TAG_subprogram ] [line 13] [local] [def] [my_strlen]
!25 = metadata !{i32 786453, i32 0, null, metadata !"", i32 0, i64 0, i64 0, i64 0, i32 0, null, metadata !26, i32 0, null, null, null} ; [ DW_TAG_subroutine_type ] [line 0, size 0, align 0, offset 0] [from ]
!26 = metadata !{metadata !8, metadata !10}
!27 = metadata !{metadata !28, metadata !29}
!28 = metadata !{i32 786689, metadata !24, metadata !"s", metadata !5, i32 16777229, metadata !10, i32 0, i32 0} ; [ DW_TAG_arg_variable ] [s] [line 13]
!29 = metadata !{i32 786688, metadata !24, metadata !"i", metadata !5, i32 14, metadata !8, i32 0, i32 0} ; [ DW_TAG_auto_variable ] [i] [line 14]
!30 = metadata !{i32 2, metadata !"Dwarf Version", i32 4}
!31 = metadata !{i32 1, metadata !"Debug Info Version", i32 1}
!32 = metadata !{metadata !"clang version 3.4 (tags/RELEASE_34/final)"}
!33 = metadata !{i32 23, i32 0, metadata !4, null}
!34 = metadata !{i32 1}
!35 = metadata !{i32 25, i32 0, metadata !36, null}
!36 = metadata !{i32 786443, metadata !1, metadata !4, i32 25, i32 0, i32 0} ; [ DW_TAG_lexical_block ] [/home/shadowvm/shadow/bupt_use_update/bupt_use/build_3/runtime/Intrinsic//home/shadowvm/shadow/bupt_use_update/bupt_use/runtime/Intrinsic/klee_mark_arg_symbolic.c]
!37 = metadata !{i32 26, i32 0, metadata !38, null}
!38 = metadata !{i32 786443, metadata !1, metadata !36, i32 25, i32 0, i32 1} ; [ DW_TAG_lexical_block ] [/home/shadowvm/shadow/bupt_use_update/bupt_use/build_3/runtime/Intrinsic//home/shadowvm/shadow/bupt_use_update/bupt_use/runtime/Intrinsic/klee_mark_arg_symbolic.c]
!39 = metadata !{metadata !40, metadata !40, i64 0}
!40 = metadata !{metadata !"any pointer", metadata !41, i64 0}
!41 = metadata !{metadata !"omnipotent char", metadata !42, i64 0}
!42 = metadata !{metadata !"Simple C/C++ TBAA"}
!43 = metadata !{i32 786689, metadata !24, metadata !"s", metadata !5, i32 16777229, metadata !10, i32 0, metadata !37} ; [ DW_TAG_arg_variable ] [s] [line 13]
!44 = metadata !{i32 13, i32 0, metadata !24, metadata !37}
!45 = metadata !{i32 786688, metadata !24, metadata !"i", metadata !5, i32 14, metadata !8, i32 0, metadata !37} ; [ DW_TAG_auto_variable ] [i] [line 14]
!46 = metadata !{i32 14, i32 0, metadata !24, metadata !37}
!47 = metadata !{i32 15, i32 0, metadata !24, metadata !37}
!48 = metadata !{metadata !41, metadata !41, i64 0}
!49 = metadata !{i32 27, i32 0, metadata !38, null}
!50 = metadata !{i32 28, i32 0, metadata !38, null}
!51 = metadata !{i32 29, i32 0, metadata !52, null}
!52 = metadata !{i32 786443, metadata !1, metadata !38, i32 29, i32 0, i32 2} ; [ DW_TAG_lexical_block ] [/home/shadowvm/shadow/bupt_use_update/bupt_use/build_3/runtime/Intrinsic//home/shadowvm/shadow/bupt_use_update/bupt_use/runtime/Intrinsic/klee_mark_arg_symbolic.c]
!53 = metadata !{i32 33, i32 0, metadata !54, null}
!54 = metadata !{i32 786443, metadata !1, metadata !52, i32 29, i32 0, i32 3} ; [ DW_TAG_lexical_block ] [/home/shadowvm/shadow/bupt_use_update/bupt_use/build_3/runtime/Intrinsic//home/shadowvm/shadow/bupt_use_update/bupt_use/runtime/Intrinsic/klee_mark_arg_symbolic.c]
!55 = metadata !{i32 786689, metadata !18, metadata !"c", metadata !5, i32 16777235, metadata !21, i32 0, metadata !53} ; [ DW_TAG_arg_variable ] [c] [line 19]
!56 = metadata !{i32 19, i32 0, metadata !18, metadata !53}
!57 = metadata !{i32 21, i32 0, metadata !18, metadata !53}
!58 = metadata !{i32 35, i32 0, metadata !38, null}
!59 = metadata !{i32 37, i32 0, metadata !4, null}
